w:World, a, b:E. FairFifo  (w_locle(w;a;b)  loc(a) = loc(b)  Id & a < b  a = b) 

latex

Definitions	t  T, x:A. B(x), FairFifo, x:AB(x), Id, w-info(w;e), e < e', left+right, x:AB(x), P & Q, P  Q, World, E, s = t, w_locl(w;x;y), P  Q, w_locle(w;x;y), P  Q, x:A. B(x), Prop, w-pred(w;e), x.A(x), pred(e), first(e), b, A, Type, A & B, rel_exp(T;R;n), f(a), , , Void, False, P  Q, x f y, R^+, R^*, {T}, SQType(T), , s ~ t, AB, {x:A| B(x) }, #$n, Dec(P), <a,b>, i=j, a<b, loc(e), True, T, IdLnk
Lemmas	squash wf, true wf, IdLnk wf, w locle wf, iff functionality wrt iff, or functionality wrt iff, w locl-lemma, w locl wf, loc wf, cless wf, Id wf, w-info wf, le wf, decidable int equal, nat wf, nat plus wf, rel exp wf, nat plus inc, not wf, assert wf, first wf, pred wf, w-pred wf, world wf, w-E wf, fair-fifo wf